Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		active(f(X,g(X),Y))	→ mark(f(Y,Y,Y))
2:		active(g(b))	→ mark(c)
3:		active(b)	→ mark(c)
4:		active(g(X))	→ g(active(X))
5:		g(mark(X))	→ mark(g(X))
6:		proper(f(X1,X2,X3))	→ f(proper(X1),proper(X2),proper(X3))
7:		proper(g(X))	→ g(proper(X))
8:		proper(b)	→ ok(b)
9:		proper(c)	→ ok(c)
10:		f(ok(X1),ok(X2),ok(X3))	→ ok(f(X1,X2,X3))
11:		g(ok(X))	→ ok(g(X))
12:		top(mark(X))	→ top(proper(X))
13:		top(ok(X))	→ top(active(X))

There are 16 dependency pairs:


14:		ACTIVE(f(X,g(X),Y))	→ F(Y,Y,Y)
15:		ACTIVE(g(X))	→ G(active(X))
16:		ACTIVE(g(X))	→ ACTIVE(X)
17:		G(mark(X))	→ G(X)
18:		PROPER(f(X1,X2,X3))	→ F(proper(X1),proper(X2),proper(X3))
19:		PROPER(f(X1,X2,X3))	→ PROPER(X1)
20:		PROPER(f(X1,X2,X3))	→ PROPER(X2)
21:		PROPER(f(X1,X2,X3))	→ PROPER(X3)
22:		PROPER(g(X))	→ G(proper(X))
23:		PROPER(g(X))	→ PROPER(X)
24:		F(ok(X1),ok(X2),ok(X3))	→ F(X1,X2,X3)
25:		G(ok(X))	→ G(X)
26:		TOP(mark(X))	→ TOP(proper(X))
27:		TOP(mark(X))	→ PROPER(X)
28:		TOP(ok(X))	→ TOP(active(X))
29:		TOP(ok(X))	→ ACTIVE(X)

The approximated dependency graph contains 5 SCCs: {24}, {17,25}, {16}, {19-21,23} and {26,28}.

Consider the SCC {24}. There are no usable rules. By taking the AF π with π(F) = 1 together with the lexicographic path order with empty precedence, rule 24 is strictly decreasing.

Consider the SCC {17,25}. There are no usable rules. By taking the AF π with π(G) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 17 is weakly decreasing and rule 25 is strictly decreasing. There is one new SCC.
- Consider the SCC {17}. By taking the AF π with π(G) = 1 together with the lexicographic path order with empty precedence, rule 17 is strictly decreasing.

Consider the SCC {16}. There are no usable rules. By taking the AF π with π(ACTIVE) = 1 together with the lexicographic path order with empty precedence, rule 16 is strictly decreasing.

Consider the SCC {19-21,23}. There are no usable rules. By taking the AF π with π(g) = π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 23 is weakly decreasing and the rules in {19-21} are strictly decreasing. There is one new SCC.
- Consider the SCC {23}. By taking the AF π with π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 23 is strictly decreasing.

Consider the SCC {26,28}. The usable rules are {1-11}. The constraints could not be solved.

Tyrolean Termination Tool (8.23 seconds) --- May 4, 2006